\begin{tabbing}
$\forall$${\it es}$:ES, $P$:(E$\rightarrow\mathbb{P}$), $p$:($\forall$$e$:E. Dec($P$($e$))), $Q$, $R$:(E$\rightarrow$E$\rightarrow\mathbb{P}$).
\\[0ex]($\forall$$x$, $y$:E. ($Q$($x$,$y$)) $\Rightarrow$ ($P$($x$) $\Leftarrow\!\Rightarrow$ $P$($y$)))
\\[0ex]$\Rightarrow$ \=(\=$\forall$$A$, $B$:Type, ${\it Ia}$:AbsInterface($A$), ${\it Ib}$:AbsInterface($B$), $f$:(E(${\it Ia}$)$\rightarrow$$B$), $g_{1}$, $g_{2}$:(E(${\it Ib}$)$\rightarrow$E),\+\+
\\[0ex]$q$:($\forall$$e$:E. Dec(($\uparrow$($e$ $\in_{b}$ ${\it Ib}$)) c$\wedge$ $P$($g_{1}$($e$)))).
\-\\[0ex]$g_{1}$ glues (${\it Ia}$$\mid$$p$):$Q$ $--$$f$$\rightarrow$ (${\it Ib}$$\mid$$q$):$R$
\\[0ex]$\Rightarrow$ $g_{2}$ glues (${\it Ia}$$\mid\neg$$p$):$Q$ $--$$f$$\rightarrow$ (${\it Ib}$$\mid\neg$$q$):$R$
\\[0ex]$\Rightarrow$ [$\lambda$$e$.$P$($g_{1}$($e$))? $g_{1}$ : $g_{2}$] glues ${\it Ia}$:$Q$ $--$$f$$\rightarrow$ ${\it Ib}$:$R$)
\-
\end{tabbing}